Three Datatype Defining Rewrite Systems for Datatypes of Integers each extending a Datatype of Naturals

摘要

Integer arithmetic is specified according to three views: unary, binary, anddecimal notation. The binary and decimal view have as their characteristic thateach normal form resembles common number notation, that is, either a digit, ora string of digits without leading zero, or the negated versions of the latter.The unary view comprises a specification of integer arithmetic based on 0,successor function $S$, and predecessor function, with negative normal forms$-S^i(0)$. Integer arithmetic in binary and decimal notation is based on(postfix) digit append functions. For each view we define a ground-confluentand terminating datatype defining rewrite system (DDRS), and in each case theresulting datatype is a canonical term algebra that extends a correspondingcanonical term algebra for natural numbers. Then, for each view, we consider an alternative DDRS based on treeconstructors that yield comparable normal forms, which for that binary anddecimal view admits expressions that are algorithmically more involved. TheseDDRSes are incorporated because they are closer to existing literature. Forthese DDRSes we also provide ground-completeness results. Finally, we define a DDRS for the ring of Integers (comprising fifteenrewrite rules) and prove its ground-completeness.